\begin{coqdoccode}
\coqdocnoindent
\coqdockw{Inductive} \coqdocvar{Id} : \coqdockw{Set} := \coqdocvar{id} : \coqdocvar{nat} \ensuremath{\rightarrow} \coqdocvar{Id}.\coqdoceol
\end{coqdoccode}
